$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id, $s$:es\_state(${\it es}$; $i$). es{-}read{-}state($s$) $\in$ es{-}state(${\it es}$; $i$)